$\vdash$  $\forall$$A$:Type, $e$:$A$, $H$:($A$$\rightarrow$Type), $z$:$H$($e$). $z$ $\neq$ 0